Nuprl Lemma : es-interface-conditional-predicate-equivalent
11,40
postcript
pdf
es
:ES,
A
:Type,
I1
,
I2
:AbsInterface(
A
). {[
I1
?
I2
]}
{
I1
}
{
I2
}
latex
Definitions
b
,
P1
P2
,
P1
P2
,
{
I
}
Lemmas
es-interface-conditional-domain-iff
origin
es:ES, A:Type, I1, I2:AbsInterface(A). {[I1?I2]} 
{I1} 
{I2} es:ES, A:Type, I1, I2:AbsInterface(A). {[I1?I2]} {I1} {I2} 
b P2 P2